//
// Created by yy N on 2022/4/15.
//
#include <iostream>
#include <fstream>
#include <string>
#include <cstdlib>
#include <unistd.h>
#include "problem.h"

Problem::Problem(int r, int c, int s): row(r), col(c), step(s) {
    numOfStateVariables = row * col * 3 * (step + 1);
    numOfActionVariables = row * col * step * 4;
    numOfVariables = numOfActionVariables + numOfStateVariables;
    pmatrix = new std::vector< std::vector<bool>>(row, std::vector<bool>(col, false));
}

void Problem::resetStep(int s){
    step = s;
    numOfStateVariables = row * col * 3 * (step + 1);
    numOfActionVariables = row * col * step * 4;
    numOfVariables = numOfActionVariables + numOfStateVariables;
    clauses.clear();
}

void Problem::initMatrix() {
    std::string inputLine;
    for(int i = 0; i<row; ++i){
        std::cin >> inputLine;
        for(int j = 0; j<col; ++j){
            if(inputLine[j] - '0' == 0)
                (*pmatrix)[i][j] = false;
            else if(inputLine[j] - '0' == 1)
                (*pmatrix)[i][j] = true;
            else{
                std::cerr << "error! The entry of the input matrix can not contain values other than 0 (for EMPTY) or 1 (for BLOCKED)\n";
                exit(-1);
            }
        }
    }
}

void Problem::initial() {
    // 设置 0 时刻的起始位置状态为 WALKER
    addClause(std::vector<int>{stateIndex(0, 0, 0, WALKER)});
    // 设置 step 时刻终点位置的状态为 WALKER
    addClause(std::vector<int>{stateIndex(row-1, col-1, step, WALKER)});
    // 这里检测一下终点位置不是墙， 如果是墙可以直接返回
    if((*pmatrix)[row-1][col-1] || (*pmatrix)[0][0] ){
        std::cout << "Key position can not be blocked, check the input.\n";
        exit(0);
    }
    for(int i = 0; i < row; ++i){
        for(int j = 0; j < col; ++j){
//            if(i == 0 && j == 0){
//                //设置之后的起始位置不能变为 block
//                for(int t = 0; t <= step; ++t){
//
//                }
//                continue;
//            }else if(i == row-1 && j == col-1){
//
//                continue;
//            }
            // 设置每个时刻的 blocked 块
            if((*pmatrix)[i][j]){
                for(int t = 0; t <= step; ++t){
                    addClause(std::vector<int>{stateIndex(i, j, t,BLOCKED)});
                }
            }else{
            // 初始空位置, 且这些位置不能变为 blocked
                for(int t = 0; t <= step; ++t){
                    addClause(std::vector<int>{-stateIndex(i, j, t,BLOCKED)});
                }
                if(!(i == 0 && j == 0)){
                    addClause(std::vector<int>{stateIndex(i, j,0,EMPTY)});
                }
            }
        }
    }
}

void Problem::uniquenessOfState(int i, int j, int t) {
    if(t <= step){
        // 至少有一个状态
        addClause(std::vector<int>{stateIndex(i, j, t, EMPTY),
                                   stateIndex(i, j, t, BLOCKED),
                                   stateIndex(i, j, t, WALKER)});
        // 最多只有一个状态: 枚举二元负文字
        addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                   -stateIndex(i, j, t, BLOCKED)});
        addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                   -stateIndex(i, j, t, WALKER)});
        addClause(std::vector<int>{-stateIndex(i, j, t, BLOCKED),
                                   -stateIndex(i, j, t, WALKER)});
    }
}

void Problem::actionConditions(int i, int j, int t) {
    if(t < step){
        // ban 出界的动作
        if( 0 == i){
            addClause(std::vector<int>{-actionIndex(i, j, t, UP)});
        }
        if( row-1 == i ){
            addClause(std::vector<int>{-actionIndex(i, j, t, DOWN)});
        }
        if( 0 == j ){
            addClause(std::vector<int>{-actionIndex(i, j, t, LEFT)});
        }
        if( col-1 == j){
            addClause(std::vector<int>{-actionIndex(i, j, t, RIGHT)});
        }
        // UP
        if( i >= 1){
            // Pre(action) 动作->产生动作的前提 （后者为前者的必要条件）
            addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                       stateIndex(i, j, t, WALKER)});
            addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                       stateIndex(i-1, j, t, EMPTY)});
            // Eff(action) 动作->该动作所产生影响 （前者为后者的充分条件）
            addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                       stateIndex(i, j, t+1, EMPTY)});
            addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                       stateIndex(i-1, j, t+1, WALKER)});
        }
        // DOWN
        if( i <= row-2){
            addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                       stateIndex(i, j, t, WALKER)});
            addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                       stateIndex(i+1, j, t, EMPTY)});

            addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                       stateIndex(i, j, t+1, EMPTY)});
            addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                       stateIndex(i+1, j, t+1, WALKER)});
        }
        // LEFT
        if( j >= 1){
            addClause(std::vector<int>{-actionIndex(i, j, t, LEFT),
                                       stateIndex(i, j, t, WALKER)});
            addClause(std::vector<int>{-actionIndex(i, j, t, LEFT),
                                       stateIndex(i, j-1, t, EMPTY)});

            addClause(std::vector<int>{-actionIndex(i, j, t, LEFT),
                                       stateIndex(i, j, t+1, EMPTY)});
            addClause(std::vector<int>{-actionIndex(i, j, t, LEFT),
                                       stateIndex(i, j-1, t+1, WALKER)});
        }
        // RIGHT
        if( j <= col-2){
            addClause(std::vector<int>{-actionIndex(i, j, t, RIGHT),
                                       stateIndex(i, j, t, WALKER)});
            addClause(std::vector<int>{-actionIndex(i, j, t, RIGHT),
                                       stateIndex(i, j+1, t, EMPTY)});

            addClause(std::vector<int>{-actionIndex(i, j, t, RIGHT),
                                       stateIndex(i, j, t+1, EMPTY)});
            addClause(std::vector<int>{-actionIndex(i, j, t, RIGHT),
                                       stateIndex(i, j+1, t+1, WALKER)});
        }

    }
}

void Problem::nessConditionOfStateChanging(int i, int j, int t) {
    if(t < step){
        if(0 == i && 0 == j){
            // 左上角的 entry
            // t 时刻 WALKER， t+1 时刻变为 EMPTY， 则发生了 下 or 右 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, RIGHT)});
            // t 时刻 EMPTY， t+1 时刻变为 WALKER， 则发生了 上 or 左 动作 且 **相邻格子需要有walker存在**
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i, j+1, t, LEFT)});
        }else if(0 == i && (col - 1) == j){
            // 右上角的 entry
            // t 时刻 WALKER， t+1 时刻变为 EMPTY， 则发生了 下 or 左 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, LEFT)});
            // t 时刻 EMPTY， t+1 时刻变为 WALKER， 则发生了 上 or 右 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i, j-1, t, RIGHT)});
        }else if((row - 1) == i && 0 == j){
            // 左下角的 entry
            // t 时刻 walker， t+1 时刻变为 EMPTY， 则发生了 UP or RIGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, RIGHT)});
            // t 时刻 empty， t+1 时刻变为 WALKER， 则发生了 DOWN or LEFT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j+1, t, LEFT)});
        }else if((row - 1) == i && (col - 1) == j){
            // 右下角的 entry
            // t 时刻 Walker， t+1 时刻变为 EMPTY， 则发生了 UP or LEFT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, LEFT)});
            // t 时刻 EMPTY， t+1 时刻变为 WALKER， 则发生了 DOWN or RIGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j-1, t, RIGHT)});
        }else if(0 == i){
            // 除角落外 第一行
            // t 时刻 W， t+1 时刻变为 EMPTY， 则发生了 DOWN or LEFT or RIGHT动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, LEFT),
                                       actionIndex(i, j, t, RIGHT)});
            // t 时刻 EM， t+1 时刻变为 WALKER， 则发生了 UP or LEFT or RIGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i, j-1, t, RIGHT),
                                       actionIndex(i, j+1, t, LEFT)});
        }else if((row - 1) == i){
            // 除角落外 最后一行
            // t 时刻 W， t+1 时刻变为 EMPTY， 则发生了 UP or LEFT or RGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, LEFT),
                                       actionIndex(i, j, t, RIGHT)});
            // t 时刻 E， t+1 时刻变为 WALKER， 则发生了 DOWN or LEFT or RIGHT动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j+1, t, LEFT),
                                       actionIndex(i, j-1, t, RIGHT)});
        }else if(0 == j){
            // 除角落外 第一列
            // t 时刻非 EMPTY， t+1 时刻变为 EMPTY， 则发生了 UP or DOWN or RIGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, RIGHT)});
            // t 时刻非 WALKER， t+1 时刻变为 WALKER， 则发生了 UP or DOWN or LEFT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j+1, t, LEFT)});
        }else if((col - 1) == j){
            // 除角落外 最后一列
            // t 时刻非 EMPTY， t+1 时刻变为 EMPTY， 则发生了 UP or DOWN or LEFT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, LEFT)});
            // t 时刻非 WALKER， t+1 时刻变为 WALKER， 则发生了 UP or DOWN or RIGHT 动作
            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j-1, t, RIGHT)});
        }else{
            // 处于矩阵中间位置的 entry, 状态发生变化的原因可以是任一动作
            addClause(std::vector<int>{-stateIndex(i, j, t, WALKER),
                                       -stateIndex(i, j, t+1, EMPTY),
                                       actionIndex(i, j, t, UP),
                                       actionIndex(i, j, t, DOWN),
                                       actionIndex(i, j, t, LEFT),
                                       actionIndex(i, j, t, RIGHT)});

            addClause(std::vector<int>{-stateIndex(i, j, t, EMPTY),
                                       -stateIndex(i, j, t+1, WALKER),
                                       actionIndex(i+1, j, t, UP),
                                       actionIndex(i-1, j, t, DOWN),
                                       actionIndex(i, j+1, t, LEFT),
                                       actionIndex(i, j-1, t, RIGHT)});
        }
    }
}

void Problem::uniquenessOfAction(int i, int j, int t) {
    if(t < step){
        // 这里不能添加东西，每个位置不一定在每一步都会有动作
//        addClause(std::vector<int>{actionIndex(i, j, t, UP),
//                                   actionIndex(i, j, t, DOWN),
//                                   actionIndex(i, j, t, LEFT),
//                                   actionIndex(i, j, t, RIGHT)});
        // 每个位置 每步 最多只有一个动作被采取
        addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                   -actionIndex(i, j, t, DOWN)});
        addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                   -actionIndex(i, j, t, LEFT)});
        addClause(std::vector<int>{-actionIndex(i, j, t, UP),
                                   -actionIndex(i, j, t, RIGHT)});
        addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                   -actionIndex(i, j, t, LEFT)});
        addClause(std::vector<int>{-actionIndex(i, j, t, DOWN),
                                   -actionIndex(i, j, t, RIGHT)});
        addClause(std::vector<int>{-actionIndex(i, j, t, LEFT),
                                   -actionIndex(i, j, t, RIGHT)});
    }
}

void Problem::genClauses() {
    initial();
    //std::cout << "initial conditions process OK\n";
    for(int i = 0; i < row; ++i){
        for(int j = 0; j < col; ++j){
            // std::cout << "processing State: " << i << " " << j <<"\n";
            for(int t = 0; t <= step; ++t){
                uniquenessOfState(i, j, t);
                actionConditions(i, j, t);
                nessConditionOfStateChanging(i, j, t);
                uniquenessOfAction(i, j, t);
            }
        }
    }
}

void Problem::saveCNF(const std::string& filename) {
    std::ofstream ofile(filename+".cnf", std::ios_base::out);
    ofile << "p cnf " << numOfVariables << " " << clauses.size() <<  std::endl;
    for (const auto& clause: clauses){
        for(auto lit: clause){
            ofile << lit <<" ";
        }
        ofile << "0\n";
    }
    ofile.close();
}

Problem::~Problem() {
    delete pmatrix;
    delete pres;
    clauses.clear();

}

void Problem::showMatrix(int x, int y) const{
    std::cout << "\n";
    for(int i = 0; i < row; ++i){
        for( int j = 0; j < col; ++j){
            if(i == x && j == y){
                std::cout << "🐢" ;
            }else if( i == row-1 && j == col-1){
                std::cout << "🚩";
            }else{
                if((*pmatrix)[i][j])
                    std::cout << "🛖" ;
                else
                    std::cout << "  ";
            }
        }
        std::cout << "\n";
    }
    std::cout << "\n";
}

bool Problem::getResult() {
    pres = new std::vector<bool>(numOfVariables+1, false);
    std::vector<bool> &res = *pres;
    std::cout << "calling Z3 for solving... \n";

    //先清空文件内容，再写入文件
    system(":> result.txt");
    system("z3 -dimacs test.cnf >> result.txt");

    //std::cout << "Done! parsing result...\n\n";
    std::ifstream streamres;
    streamres.open("result.txt");
    if(! streamres.is_open()){
        std::cerr << "err when open 'result.txt'!\n";
        exit(-1);
    }
    std::string tmp;
    streamres >> tmp;
    if(tmp == "s"){
        streamres >> tmp;
        if(tmp == "SATISFIABLE"){
            std::cout << "SAT!\n";
            streamres >> tmp;
            // std::cout << "tmp: " << tmp << std::endl;
            // std::cout << "reading variables \n";
            for(int i = 1; i <= numOfVariables; ++i){
                int tmpInt = 0;
                streamres >> tmpInt;
                res[i] = tmpInt > 0;
            }
            streamres.close();
            return true;
        }
        else{
            std::cout << "UNSAT! step: "<< step <<"\n";
            streamres.close();
            return false;
        }
    }else{
        std::cerr << "Something wrong happened during Z3 solving (output file: \"result.txt\", Check it out)\n";
        streamres.close();
        exit(-1);
    }
}

void Problem::parseResult(){
    std::cout << "Minimum step satisfy p: " << step <<"\n";

    std::vector<bool> &res = *pres;
    for(int t = 0; t < step; ++t){
        //sleep(1);
        //system("clear");
        std::cout << "step: " << t <<"\n";
        for(int i = 0; i < row; ++i){
            for(int j = 0; j < col; ++j){
                if(res[stateIndex(i, j, t, WALKER)]){
                    showMatrix(i, j);
                }
                if(res[actionIndex(i, j, t, UP)]){
                    std::cout << "action UP: from " << i << ", " << j << "\n";
                }
                if(res[actionIndex(i, j, t, DOWN)]){
                    std::cout << "action DOWN: from " << i << ", " << j << "\n";
                }
                if(res[actionIndex(i, j, t, LEFT)]){
                    std::cout << "action LEFT: from " << i << ", " << j << "\n";
                }
                if(res[actionIndex(i, j, t, RIGHT)]){
                    std::cout << "action RIGHT: from " << i << ", " << j << "\n";
                }
            }
        }
    }
    //sleep(1);
    //system("clear");
    showMatrix(row-1, col-1);
    std::cout << "Parse over\n";
}

void Problem::showMoving(std::vector<bool> &res) const {
    for(int t = 0; t <= step; ++t){
        std::cout << "step: " << t << "\n";
        for(int i = 0; i<row; ++i){
            for(int j = 0; j <col; ++j){
                if(res[stateIndex(i, j, t, WALKER)]){
                    //std::cout << i << " " << j << " " << t << " " << "walker\n";
                    std::cout << "w";
                }else if(res[stateIndex(i, j, t, EMPTY)]){
                    std::cout << " ";
                }else if(res[stateIndex(i, j, t, BLOCKED)]){
                    std::cout << "b";
                }else{
                    std::cout << " ";
                }
                if(t < step){
                    if(res[actionIndex(i, j, t, UP)]){
                        std::cout << "U";
                    }else if(res[actionIndex(i, j, t, DOWN)]){
                        std::cout << "D";
                    }else if(res[actionIndex(i, j, t, LEFT)]){
                        std::cout << "L";
                    }else if(res[actionIndex(i, j, t, RIGHT)]){
                        std::cout << "R";
                    }else{
                        std::cout << " ";
                    }
                }else{
                    std::cout << " ";
                }
            }
            std::cout << "\n";
        }
    }
}

void Problem::printInfo() {
    std::cout << "Size of problem, row: " << row << ", col: " << col << ", step: " << step << std::endl;
    std::cout << "Number of variables: " << numOfVariables << std::endl;
    std::cout << "Number of state variables: " << numOfStateVariables << std::endl;
    std::cout << "Number of action variables: " << numOfActionVariables << std::endl;
    std::cout << "Number of clauses: " << clauses.size() << std::endl;
}


